Left Termination of the query pattern
goal(g,a,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 375 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 293 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 7 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES

(0) Obligation:

Clauses:

goal(A, B, C) :- ','(s2t(A, T), tapplast(T, B, C)).
tapplast(L, X, Last) :- ','(tappend(L, node(nil, X, nil), LX), tlast(Last, LX)).
tlast(X, node(nil, X, nil)).
tlast(X, node(L, H, R)) :- tlast(X, L).
tlast(X, node(L, H, R)) :- tlast(X, R).
tappend(nil, T, T).
tappend(node(nil, X, T2), T1, node(T1, X, T2)).
tappend(node(T1, X, nil), T2, node(T1, X, T2)).
tappend(node(T1, X, T2), T3, node(U, X, T2)) :- tappend(T1, T3, U).
tappend(node(T1, X, T2), T3, node(T1, X, U)) :- tappend(T2, T3, U).
s2t(s(X), node(T, Y, T)) :- s2t(X, T).
s2t(s(X), node(nil, Y, T)) :- s2t(X, T).
s2t(s(X), node(T, Y, nil)) :- s2t(X, T).
s2t(s(X), node(nil, Y, nil)).
s2t(0, nil).

Query: goal(g,a,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

s2tA(s(X1), node(X2, X3, X2)) :- s2tA(X1, X2).
s2tA(s(X1), node(nil, X2, X3)) :- s2tA(X1, X3).
s2tA(s(X1), node(X2, X3, nil)) :- s2tA(X1, X2).
tappendB(node(X1, X2, X3), X4, node(X5, X2, X3)) :- tappendB(X1, X4, X5).
tappendB(node(X1, X2, X3), X4, node(X1, X2, X5)) :- tappendB(X3, X4, X5).
tlastC(X1, node(X2, X3, X4)) :- tlastC(X1, X2).
tlastC(X1, node(X2, X3, X4)) :- tlastC(X1, X4).
goalF(s(X1), X2, X3) :- s2tA(X1, X4).
goalF(s(X1), X2, X3) :- ','(s2tcA(X1, X4), tappendB(X4, X2, X5)).
goalF(s(X1), X2, X3) :- ','(s2tcA(X1, X4), tappendB(X4, X2, X5)).
goalF(s(X1), X2, X3) :- ','(s2tcA(X1, X4), ','(tappendcD(X4, X5, X2, X6), tlastC(X3, X6))).
goalF(s(X1), X2, X3) :- s2tA(X1, X4).
goalF(s(X1), X2, X3) :- ','(s2tcA(X1, X4), tappendB(node(nil, X5, X4), X2, X6)).
goalF(s(X1), X2, X3) :- ','(s2tcA(X1, X4), ','(tappendcB(node(nil, X5, X4), X2, X6), tlastC(X3, X6))).
goalF(s(X1), X2, X3) :- s2tA(X1, X4).
goalF(s(X1), X2, X3) :- ','(s2tcA(X1, X4), tappendB(node(X4, X5, nil), X2, X6)).
goalF(s(X1), X2, X3) :- ','(s2tcA(X1, X4), ','(tappendcB(node(X4, X5, nil), X2, X6), tlastC(X3, X6))).
goalF(s(X1), X2, X3) :- tappendB(node(nil, X4, nil), X2, X5).
goalF(s(X1), X2, X3) :- ','(tappendcB(node(nil, X4, nil), X2, X5), tlastC(X3, X5)).
goalF(0, X1, X2) :- ','(tappendcE(X1, X3), tlastC(X2, X3)).

Clauses:

s2tcA(s(X1), node(X2, X3, X2)) :- s2tcA(X1, X2).
s2tcA(s(X1), node(nil, X2, X3)) :- s2tcA(X1, X3).
s2tcA(s(X1), node(X2, X3, nil)) :- s2tcA(X1, X2).
s2tcA(s(X1), node(nil, X2, nil)).
s2tcA(0, nil).
tappendcB(nil, X1, node(nil, X1, nil)).
tappendcB(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2)).
tappendcB(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil))).
tappendcB(node(X1, X2, X3), X4, node(X5, X2, X3)) :- tappendcB(X1, X4, X5).
tappendcB(node(X1, X2, X3), X4, node(X1, X2, X5)) :- tappendcB(X3, X4, X5).
tlastcC(X1, node(nil, X1, nil)).
tlastcC(X1, node(X2, X3, X4)) :- tlastcC(X1, X2).
tlastcC(X1, node(X2, X3, X4)) :- tlastcC(X1, X4).
tappendcD(nil, X1, X2, node(node(nil, X2, nil), X1, nil)).
tappendcD(nil, X1, X2, node(nil, X1, node(nil, X2, nil))).
tappendcD(X1, X2, X3, node(X4, X2, X1)) :- tappendcB(X1, X3, X4).
tappendcD(X1, X2, X3, node(X1, X2, X4)) :- tappendcB(X1, X3, X4).
tappendcE(X1, node(nil, X1, nil)).

Afs:

goalF(x1, x2, x3)  =  goalF(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
goalF_in: (b,f,f)
s2tA_in: (b,f)
s2tcA_in: (b,f)
tappendB_in: (b,f,f)
tappendcD_in: (b,f,f,f)
tappendcB_in: (b,f,f)
tlastC_in: (f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOALF_IN_GAA(s(X1), X2, X3) → U8_GAA(X1, X2, X3, s2tA_in_ga(X1, X4))
GOALF_IN_GAA(s(X1), X2, X3) → S2TA_IN_GA(X1, X4)
S2TA_IN_GA(s(X1), node(X2, X3, X2)) → U1_GA(X1, X2, X3, s2tA_in_ga(X1, X2))
S2TA_IN_GA(s(X1), node(X2, X3, X2)) → S2TA_IN_GA(X1, X2)
S2TA_IN_GA(s(X1), node(nil, X2, X3)) → U2_GA(X1, X2, X3, s2tA_in_ga(X1, X3))
S2TA_IN_GA(s(X1), node(nil, X2, X3)) → S2TA_IN_GA(X1, X3)
S2TA_IN_GA(s(X1), node(X2, X3, nil)) → U3_GA(X1, X2, X3, s2tA_in_ga(X1, X2))
S2TA_IN_GA(s(X1), node(X2, X3, nil)) → S2TA_IN_GA(X1, X2)
GOALF_IN_GAA(s(X1), X2, X3) → U9_GAA(X1, X2, X3, s2tcA_in_ga(X1, X4))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U10_GAA(X1, X2, X3, tappendB_in_gaa(X4, X2, X5))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → TAPPENDB_IN_GAA(X4, X2, X5)
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X5, X2, X3)) → U4_GAA(X1, X2, X3, X4, X5, tappendB_in_gaa(X1, X4, X5))
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X5, X2, X3)) → TAPPENDB_IN_GAA(X1, X4, X5)
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X1, X2, X5)) → U5_GAA(X1, X2, X3, X4, X5, tappendB_in_gaa(X3, X4, X5))
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X1, X2, X5)) → TAPPENDB_IN_GAA(X3, X4, X5)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U11_GAA(X1, X2, X3, tappendcD_in_gaaa(X4, X5, X2, X6))
U11_GAA(X1, X2, X3, tappendcD_out_gaaa(X4, X5, X2, X6)) → U12_GAA(X1, X2, X3, tlastC_in_ag(X3, X6))
U11_GAA(X1, X2, X3, tappendcD_out_gaaa(X4, X5, X2, X6)) → TLASTC_IN_AG(X3, X6)
TLASTC_IN_AG(X1, node(X2, X3, X4)) → U6_AG(X1, X2, X3, X4, tlastC_in_ag(X1, X2))
TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X2)
TLASTC_IN_AG(X1, node(X2, X3, X4)) → U7_AG(X1, X2, X3, X4, tlastC_in_ag(X1, X4))
TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X4)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U13_GAA(X1, X2, X3, tappendB_in_gaa(node(nil, X5, X4), X2, X6))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → TAPPENDB_IN_GAA(node(nil, X5, X4), X2, X6)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U14_GAA(X1, X2, X3, tappendcB_in_gaa(node(nil, X5, X4), X2, X6))
U14_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X5, X4), X2, X6)) → U15_GAA(X1, X2, X3, tlastC_in_ag(X3, X6))
U14_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X5, X4), X2, X6)) → TLASTC_IN_AG(X3, X6)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U16_GAA(X1, X2, X3, tappendB_in_gaa(node(X4, X5, nil), X2, X6))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → TAPPENDB_IN_GAA(node(X4, X5, nil), X2, X6)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U17_GAA(X1, X2, X3, tappendcB_in_gaa(node(X4, X5, nil), X2, X6))
U17_GAA(X1, X2, X3, tappendcB_out_gaa(node(X4, X5, nil), X2, X6)) → U18_GAA(X1, X2, X3, tlastC_in_ag(X3, X6))
U17_GAA(X1, X2, X3, tappendcB_out_gaa(node(X4, X5, nil), X2, X6)) → TLASTC_IN_AG(X3, X6)
GOALF_IN_GAA(s(X1), X2, X3) → U19_GAA(X1, X2, X3, tappendB_in_gaa(node(nil, X4, nil), X2, X5))
GOALF_IN_GAA(s(X1), X2, X3) → TAPPENDB_IN_GAA(node(nil, X4, nil), X2, X5)
GOALF_IN_GAA(s(X1), X2, X3) → U20_GAA(X1, X2, X3, tappendcB_in_gaa(node(nil, X4, nil), X2, X5))
U20_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X4, nil), X2, X5)) → U21_GAA(X1, X2, X3, tlastC_in_ag(X3, X5))
U20_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X4, nil), X2, X5)) → TLASTC_IN_AG(X3, X5)
GOALF_IN_GAA(0, X1, X2) → U22_GAA(X1, X2, tappendcE_in_aa(X1, X3))
U22_GAA(X1, X2, tappendcE_out_aa(X1, X3)) → U23_GAA(X1, X2, tlastC_in_ag(X2, X3))
U22_GAA(X1, X2, tappendcE_out_aa(X1, X3)) → TLASTC_IN_AG(X2, X3)

The TRS R consists of the following rules:

s2tcA_in_ga(s(X1), node(X2, X3, X2)) → U25_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, X3)) → U26_ga(X1, X2, X3, s2tcA_in_ga(X1, X3))
s2tcA_in_ga(s(X1), node(X2, X3, nil)) → U27_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, nil)) → s2tcA_out_ga(s(X1), node(nil, X2, nil))
s2tcA_in_ga(0, nil) → s2tcA_out_ga(0, nil)
U27_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, nil))
U26_ga(X1, X2, X3, s2tcA_out_ga(X1, X3)) → s2tcA_out_ga(s(X1), node(nil, X2, X3))
U25_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, X2))
tappendcD_in_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil)) → tappendcD_out_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil))
tappendcD_in_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil))) → tappendcD_out_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil)))
tappendcD_in_gaaa(X1, X2, X3, node(X4, X2, X1)) → U32_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
tappendcB_in_gaa(nil, X1, node(nil, X1, nil)) → tappendcB_out_gaa(nil, X1, node(nil, X1, nil))
tappendcB_in_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2)) → tappendcB_out_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2))
tappendcB_in_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil))) → tappendcB_out_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil)))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X5, X2, X3)) → U28_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X1, X4, X5))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X1, X2, X5)) → U29_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X3, X4, X5))
U29_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X3, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X1, X2, X5))
U28_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X1, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X5, X2, X3))
U32_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X4, X2, X1))
tappendcD_in_gaaa(X1, X2, X3, node(X1, X2, X4)) → U33_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
U33_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X1, X2, X4))
tappendcE_in_aa(X1, node(nil, X1, nil)) → tappendcE_out_aa(X1, node(nil, X1, nil))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2tA_in_ga(x1, x2)  =  s2tA_in_ga(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tcA_in_ga(x1, x2)  =  s2tcA_in_ga(x1)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x1, x4)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x1, x4)
s2tcA_out_ga(x1, x2)  =  s2tcA_out_ga(x1, x2)
0  =  0
tappendB_in_gaa(x1, x2, x3)  =  tappendB_in_gaa(x1)
tappendcD_in_gaaa(x1, x2, x3, x4)  =  tappendcD_in_gaaa(x1)
nil  =  nil
tappendcD_out_gaaa(x1, x2, x3, x4)  =  tappendcD_out_gaaa(x1, x4)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
tappendcB_in_gaa(x1, x2, x3)  =  tappendcB_in_gaa(x1)
tappendcB_out_gaa(x1, x2, x3)  =  tappendcB_out_gaa(x1, x3)
U28_gaa(x1, x2, x3, x4, x5, x6)  =  U28_gaa(x1, x3, x6)
U29_gaa(x1, x2, x3, x4, x5, x6)  =  U29_gaa(x1, x3, x6)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x5)
tlastC_in_ag(x1, x2)  =  tlastC_in_ag(x2)
tappendcE_in_aa(x1, x2)  =  tappendcE_in_aa
tappendcE_out_aa(x1, x2)  =  tappendcE_out_aa(x2)
GOALF_IN_GAA(x1, x2, x3)  =  GOALF_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4)  =  U8_GAA(x1, x4)
S2TA_IN_GA(x1, x2)  =  S2TA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x1, x4)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
TAPPENDB_IN_GAA(x1, x2, x3)  =  TAPPENDB_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6)  =  U4_GAA(x1, x3, x6)
U5_GAA(x1, x2, x3, x4, x5, x6)  =  U5_GAA(x1, x3, x6)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x4)
U12_GAA(x1, x2, x3, x4)  =  U12_GAA(x1, x4)
TLASTC_IN_AG(x1, x2)  =  TLASTC_IN_AG(x2)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x2, x4, x5)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x2, x4, x5)
U13_GAA(x1, x2, x3, x4)  =  U13_GAA(x1, x4)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x4)
U15_GAA(x1, x2, x3, x4)  =  U15_GAA(x1, x4)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x4)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x4)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x4)
U22_GAA(x1, x2, x3)  =  U22_GAA(x3)
U23_GAA(x1, x2, x3)  =  U23_GAA(x3)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GOALF_IN_GAA(s(X1), X2, X3) → U8_GAA(X1, X2, X3, s2tA_in_ga(X1, X4))
GOALF_IN_GAA(s(X1), X2, X3) → S2TA_IN_GA(X1, X4)
S2TA_IN_GA(s(X1), node(X2, X3, X2)) → U1_GA(X1, X2, X3, s2tA_in_ga(X1, X2))
S2TA_IN_GA(s(X1), node(X2, X3, X2)) → S2TA_IN_GA(X1, X2)
S2TA_IN_GA(s(X1), node(nil, X2, X3)) → U2_GA(X1, X2, X3, s2tA_in_ga(X1, X3))
S2TA_IN_GA(s(X1), node(nil, X2, X3)) → S2TA_IN_GA(X1, X3)
S2TA_IN_GA(s(X1), node(X2, X3, nil)) → U3_GA(X1, X2, X3, s2tA_in_ga(X1, X2))
S2TA_IN_GA(s(X1), node(X2, X3, nil)) → S2TA_IN_GA(X1, X2)
GOALF_IN_GAA(s(X1), X2, X3) → U9_GAA(X1, X2, X3, s2tcA_in_ga(X1, X4))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U10_GAA(X1, X2, X3, tappendB_in_gaa(X4, X2, X5))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → TAPPENDB_IN_GAA(X4, X2, X5)
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X5, X2, X3)) → U4_GAA(X1, X2, X3, X4, X5, tappendB_in_gaa(X1, X4, X5))
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X5, X2, X3)) → TAPPENDB_IN_GAA(X1, X4, X5)
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X1, X2, X5)) → U5_GAA(X1, X2, X3, X4, X5, tappendB_in_gaa(X3, X4, X5))
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X1, X2, X5)) → TAPPENDB_IN_GAA(X3, X4, X5)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U11_GAA(X1, X2, X3, tappendcD_in_gaaa(X4, X5, X2, X6))
U11_GAA(X1, X2, X3, tappendcD_out_gaaa(X4, X5, X2, X6)) → U12_GAA(X1, X2, X3, tlastC_in_ag(X3, X6))
U11_GAA(X1, X2, X3, tappendcD_out_gaaa(X4, X5, X2, X6)) → TLASTC_IN_AG(X3, X6)
TLASTC_IN_AG(X1, node(X2, X3, X4)) → U6_AG(X1, X2, X3, X4, tlastC_in_ag(X1, X2))
TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X2)
TLASTC_IN_AG(X1, node(X2, X3, X4)) → U7_AG(X1, X2, X3, X4, tlastC_in_ag(X1, X4))
TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X4)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U13_GAA(X1, X2, X3, tappendB_in_gaa(node(nil, X5, X4), X2, X6))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → TAPPENDB_IN_GAA(node(nil, X5, X4), X2, X6)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U14_GAA(X1, X2, X3, tappendcB_in_gaa(node(nil, X5, X4), X2, X6))
U14_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X5, X4), X2, X6)) → U15_GAA(X1, X2, X3, tlastC_in_ag(X3, X6))
U14_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X5, X4), X2, X6)) → TLASTC_IN_AG(X3, X6)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U16_GAA(X1, X2, X3, tappendB_in_gaa(node(X4, X5, nil), X2, X6))
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → TAPPENDB_IN_GAA(node(X4, X5, nil), X2, X6)
U9_GAA(X1, X2, X3, s2tcA_out_ga(X1, X4)) → U17_GAA(X1, X2, X3, tappendcB_in_gaa(node(X4, X5, nil), X2, X6))
U17_GAA(X1, X2, X3, tappendcB_out_gaa(node(X4, X5, nil), X2, X6)) → U18_GAA(X1, X2, X3, tlastC_in_ag(X3, X6))
U17_GAA(X1, X2, X3, tappendcB_out_gaa(node(X4, X5, nil), X2, X6)) → TLASTC_IN_AG(X3, X6)
GOALF_IN_GAA(s(X1), X2, X3) → U19_GAA(X1, X2, X3, tappendB_in_gaa(node(nil, X4, nil), X2, X5))
GOALF_IN_GAA(s(X1), X2, X3) → TAPPENDB_IN_GAA(node(nil, X4, nil), X2, X5)
GOALF_IN_GAA(s(X1), X2, X3) → U20_GAA(X1, X2, X3, tappendcB_in_gaa(node(nil, X4, nil), X2, X5))
U20_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X4, nil), X2, X5)) → U21_GAA(X1, X2, X3, tlastC_in_ag(X3, X5))
U20_GAA(X1, X2, X3, tappendcB_out_gaa(node(nil, X4, nil), X2, X5)) → TLASTC_IN_AG(X3, X5)
GOALF_IN_GAA(0, X1, X2) → U22_GAA(X1, X2, tappendcE_in_aa(X1, X3))
U22_GAA(X1, X2, tappendcE_out_aa(X1, X3)) → U23_GAA(X1, X2, tlastC_in_ag(X2, X3))
U22_GAA(X1, X2, tappendcE_out_aa(X1, X3)) → TLASTC_IN_AG(X2, X3)

The TRS R consists of the following rules:

s2tcA_in_ga(s(X1), node(X2, X3, X2)) → U25_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, X3)) → U26_ga(X1, X2, X3, s2tcA_in_ga(X1, X3))
s2tcA_in_ga(s(X1), node(X2, X3, nil)) → U27_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, nil)) → s2tcA_out_ga(s(X1), node(nil, X2, nil))
s2tcA_in_ga(0, nil) → s2tcA_out_ga(0, nil)
U27_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, nil))
U26_ga(X1, X2, X3, s2tcA_out_ga(X1, X3)) → s2tcA_out_ga(s(X1), node(nil, X2, X3))
U25_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, X2))
tappendcD_in_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil)) → tappendcD_out_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil))
tappendcD_in_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil))) → tappendcD_out_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil)))
tappendcD_in_gaaa(X1, X2, X3, node(X4, X2, X1)) → U32_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
tappendcB_in_gaa(nil, X1, node(nil, X1, nil)) → tappendcB_out_gaa(nil, X1, node(nil, X1, nil))
tappendcB_in_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2)) → tappendcB_out_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2))
tappendcB_in_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil))) → tappendcB_out_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil)))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X5, X2, X3)) → U28_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X1, X4, X5))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X1, X2, X5)) → U29_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X3, X4, X5))
U29_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X3, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X1, X2, X5))
U28_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X1, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X5, X2, X3))
U32_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X4, X2, X1))
tappendcD_in_gaaa(X1, X2, X3, node(X1, X2, X4)) → U33_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
U33_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X1, X2, X4))
tappendcE_in_aa(X1, node(nil, X1, nil)) → tappendcE_out_aa(X1, node(nil, X1, nil))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2tA_in_ga(x1, x2)  =  s2tA_in_ga(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tcA_in_ga(x1, x2)  =  s2tcA_in_ga(x1)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x1, x4)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x1, x4)
s2tcA_out_ga(x1, x2)  =  s2tcA_out_ga(x1, x2)
0  =  0
tappendB_in_gaa(x1, x2, x3)  =  tappendB_in_gaa(x1)
tappendcD_in_gaaa(x1, x2, x3, x4)  =  tappendcD_in_gaaa(x1)
nil  =  nil
tappendcD_out_gaaa(x1, x2, x3, x4)  =  tappendcD_out_gaaa(x1, x4)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
tappendcB_in_gaa(x1, x2, x3)  =  tappendcB_in_gaa(x1)
tappendcB_out_gaa(x1, x2, x3)  =  tappendcB_out_gaa(x1, x3)
U28_gaa(x1, x2, x3, x4, x5, x6)  =  U28_gaa(x1, x3, x6)
U29_gaa(x1, x2, x3, x4, x5, x6)  =  U29_gaa(x1, x3, x6)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x5)
tlastC_in_ag(x1, x2)  =  tlastC_in_ag(x2)
tappendcE_in_aa(x1, x2)  =  tappendcE_in_aa
tappendcE_out_aa(x1, x2)  =  tappendcE_out_aa(x2)
GOALF_IN_GAA(x1, x2, x3)  =  GOALF_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4)  =  U8_GAA(x1, x4)
S2TA_IN_GA(x1, x2)  =  S2TA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U9_GAA(x1, x2, x3, x4)  =  U9_GAA(x1, x4)
U10_GAA(x1, x2, x3, x4)  =  U10_GAA(x1, x4)
TAPPENDB_IN_GAA(x1, x2, x3)  =  TAPPENDB_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6)  =  U4_GAA(x1, x3, x6)
U5_GAA(x1, x2, x3, x4, x5, x6)  =  U5_GAA(x1, x3, x6)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x4)
U12_GAA(x1, x2, x3, x4)  =  U12_GAA(x1, x4)
TLASTC_IN_AG(x1, x2)  =  TLASTC_IN_AG(x2)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x2, x4, x5)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x2, x4, x5)
U13_GAA(x1, x2, x3, x4)  =  U13_GAA(x1, x4)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x4)
U15_GAA(x1, x2, x3, x4)  =  U15_GAA(x1, x4)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x4)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x4)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x4)
U22_GAA(x1, x2, x3)  =  U22_GAA(x3)
U23_GAA(x1, x2, x3)  =  U23_GAA(x3)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 33 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X4)
TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X2)

The TRS R consists of the following rules:

s2tcA_in_ga(s(X1), node(X2, X3, X2)) → U25_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, X3)) → U26_ga(X1, X2, X3, s2tcA_in_ga(X1, X3))
s2tcA_in_ga(s(X1), node(X2, X3, nil)) → U27_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, nil)) → s2tcA_out_ga(s(X1), node(nil, X2, nil))
s2tcA_in_ga(0, nil) → s2tcA_out_ga(0, nil)
U27_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, nil))
U26_ga(X1, X2, X3, s2tcA_out_ga(X1, X3)) → s2tcA_out_ga(s(X1), node(nil, X2, X3))
U25_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, X2))
tappendcD_in_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil)) → tappendcD_out_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil))
tappendcD_in_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil))) → tappendcD_out_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil)))
tappendcD_in_gaaa(X1, X2, X3, node(X4, X2, X1)) → U32_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
tappendcB_in_gaa(nil, X1, node(nil, X1, nil)) → tappendcB_out_gaa(nil, X1, node(nil, X1, nil))
tappendcB_in_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2)) → tappendcB_out_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2))
tappendcB_in_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil))) → tappendcB_out_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil)))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X5, X2, X3)) → U28_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X1, X4, X5))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X1, X2, X5)) → U29_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X3, X4, X5))
U29_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X3, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X1, X2, X5))
U28_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X1, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X5, X2, X3))
U32_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X4, X2, X1))
tappendcD_in_gaaa(X1, X2, X3, node(X1, X2, X4)) → U33_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
U33_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X1, X2, X4))
tappendcE_in_aa(X1, node(nil, X1, nil)) → tappendcE_out_aa(X1, node(nil, X1, nil))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tcA_in_ga(x1, x2)  =  s2tcA_in_ga(x1)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x1, x4)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x1, x4)
s2tcA_out_ga(x1, x2)  =  s2tcA_out_ga(x1, x2)
0  =  0
tappendcD_in_gaaa(x1, x2, x3, x4)  =  tappendcD_in_gaaa(x1)
nil  =  nil
tappendcD_out_gaaa(x1, x2, x3, x4)  =  tappendcD_out_gaaa(x1, x4)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
tappendcB_in_gaa(x1, x2, x3)  =  tappendcB_in_gaa(x1)
tappendcB_out_gaa(x1, x2, x3)  =  tappendcB_out_gaa(x1, x3)
U28_gaa(x1, x2, x3, x4, x5, x6)  =  U28_gaa(x1, x3, x6)
U29_gaa(x1, x2, x3, x4, x5, x6)  =  U29_gaa(x1, x3, x6)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x5)
tappendcE_in_aa(x1, x2)  =  tappendcE_in_aa
tappendcE_out_aa(x1, x2)  =  tappendcE_out_aa(x2)
TLASTC_IN_AG(x1, x2)  =  TLASTC_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X4)
TLASTC_IN_AG(X1, node(X2, X3, X4)) → TLASTC_IN_AG(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
node(x1, x2, x3)  =  node(x1, x3)
TLASTC_IN_AG(x1, x2)  =  TLASTC_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TLASTC_IN_AG(node(X2, X4)) → TLASTC_IN_AG(X4)
TLASTC_IN_AG(node(X2, X4)) → TLASTC_IN_AG(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • TLASTC_IN_AG(node(X2, X4)) → TLASTC_IN_AG(X4)
    The graph contains the following edges 1 > 1

  • TLASTC_IN_AG(node(X2, X4)) → TLASTC_IN_AG(X2)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X1, X2, X5)) → TAPPENDB_IN_GAA(X3, X4, X5)
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X5, X2, X3)) → TAPPENDB_IN_GAA(X1, X4, X5)

The TRS R consists of the following rules:

s2tcA_in_ga(s(X1), node(X2, X3, X2)) → U25_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, X3)) → U26_ga(X1, X2, X3, s2tcA_in_ga(X1, X3))
s2tcA_in_ga(s(X1), node(X2, X3, nil)) → U27_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, nil)) → s2tcA_out_ga(s(X1), node(nil, X2, nil))
s2tcA_in_ga(0, nil) → s2tcA_out_ga(0, nil)
U27_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, nil))
U26_ga(X1, X2, X3, s2tcA_out_ga(X1, X3)) → s2tcA_out_ga(s(X1), node(nil, X2, X3))
U25_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, X2))
tappendcD_in_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil)) → tappendcD_out_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil))
tappendcD_in_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil))) → tappendcD_out_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil)))
tappendcD_in_gaaa(X1, X2, X3, node(X4, X2, X1)) → U32_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
tappendcB_in_gaa(nil, X1, node(nil, X1, nil)) → tappendcB_out_gaa(nil, X1, node(nil, X1, nil))
tappendcB_in_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2)) → tappendcB_out_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2))
tappendcB_in_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil))) → tappendcB_out_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil)))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X5, X2, X3)) → U28_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X1, X4, X5))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X1, X2, X5)) → U29_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X3, X4, X5))
U29_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X3, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X1, X2, X5))
U28_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X1, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X5, X2, X3))
U32_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X4, X2, X1))
tappendcD_in_gaaa(X1, X2, X3, node(X1, X2, X4)) → U33_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
U33_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X1, X2, X4))
tappendcE_in_aa(X1, node(nil, X1, nil)) → tappendcE_out_aa(X1, node(nil, X1, nil))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tcA_in_ga(x1, x2)  =  s2tcA_in_ga(x1)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x1, x4)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x1, x4)
s2tcA_out_ga(x1, x2)  =  s2tcA_out_ga(x1, x2)
0  =  0
tappendcD_in_gaaa(x1, x2, x3, x4)  =  tappendcD_in_gaaa(x1)
nil  =  nil
tappendcD_out_gaaa(x1, x2, x3, x4)  =  tappendcD_out_gaaa(x1, x4)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
tappendcB_in_gaa(x1, x2, x3)  =  tappendcB_in_gaa(x1)
tappendcB_out_gaa(x1, x2, x3)  =  tappendcB_out_gaa(x1, x3)
U28_gaa(x1, x2, x3, x4, x5, x6)  =  U28_gaa(x1, x3, x6)
U29_gaa(x1, x2, x3, x4, x5, x6)  =  U29_gaa(x1, x3, x6)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x5)
tappendcE_in_aa(x1, x2)  =  tappendcE_in_aa
tappendcE_out_aa(x1, x2)  =  tappendcE_out_aa(x2)
TAPPENDB_IN_GAA(x1, x2, x3)  =  TAPPENDB_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X1, X2, X5)) → TAPPENDB_IN_GAA(X3, X4, X5)
TAPPENDB_IN_GAA(node(X1, X2, X3), X4, node(X5, X2, X3)) → TAPPENDB_IN_GAA(X1, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
node(x1, x2, x3)  =  node(x1, x3)
TAPPENDB_IN_GAA(x1, x2, x3)  =  TAPPENDB_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TAPPENDB_IN_GAA(node(X1, X3)) → TAPPENDB_IN_GAA(X3)
TAPPENDB_IN_GAA(node(X1, X3)) → TAPPENDB_IN_GAA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • TAPPENDB_IN_GAA(node(X1, X3)) → TAPPENDB_IN_GAA(X3)
    The graph contains the following edges 1 > 1

  • TAPPENDB_IN_GAA(node(X1, X3)) → TAPPENDB_IN_GAA(X1)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

S2TA_IN_GA(s(X1), node(nil, X2, X3)) → S2TA_IN_GA(X1, X3)
S2TA_IN_GA(s(X1), node(X2, X3, X2)) → S2TA_IN_GA(X1, X2)
S2TA_IN_GA(s(X1), node(X2, X3, nil)) → S2TA_IN_GA(X1, X2)

The TRS R consists of the following rules:

s2tcA_in_ga(s(X1), node(X2, X3, X2)) → U25_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, X3)) → U26_ga(X1, X2, X3, s2tcA_in_ga(X1, X3))
s2tcA_in_ga(s(X1), node(X2, X3, nil)) → U27_ga(X1, X2, X3, s2tcA_in_ga(X1, X2))
s2tcA_in_ga(s(X1), node(nil, X2, nil)) → s2tcA_out_ga(s(X1), node(nil, X2, nil))
s2tcA_in_ga(0, nil) → s2tcA_out_ga(0, nil)
U27_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, nil))
U26_ga(X1, X2, X3, s2tcA_out_ga(X1, X3)) → s2tcA_out_ga(s(X1), node(nil, X2, X3))
U25_ga(X1, X2, X3, s2tcA_out_ga(X1, X2)) → s2tcA_out_ga(s(X1), node(X2, X3, X2))
tappendcD_in_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil)) → tappendcD_out_gaaa(nil, X1, X2, node(node(nil, X2, nil), X1, nil))
tappendcD_in_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil))) → tappendcD_out_gaaa(nil, X1, X2, node(nil, X1, node(nil, X2, nil)))
tappendcD_in_gaaa(X1, X2, X3, node(X4, X2, X1)) → U32_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
tappendcB_in_gaa(nil, X1, node(nil, X1, nil)) → tappendcB_out_gaa(nil, X1, node(nil, X1, nil))
tappendcB_in_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2)) → tappendcB_out_gaa(node(nil, X1, X2), X3, node(node(nil, X3, nil), X1, X2))
tappendcB_in_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil))) → tappendcB_out_gaa(node(X1, X2, nil), X3, node(X1, X2, node(nil, X3, nil)))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X5, X2, X3)) → U28_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X1, X4, X5))
tappendcB_in_gaa(node(X1, X2, X3), X4, node(X1, X2, X5)) → U29_gaa(X1, X2, X3, X4, X5, tappendcB_in_gaa(X3, X4, X5))
U29_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X3, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X1, X2, X5))
U28_gaa(X1, X2, X3, X4, X5, tappendcB_out_gaa(X1, X4, X5)) → tappendcB_out_gaa(node(X1, X2, X3), X4, node(X5, X2, X3))
U32_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X4, X2, X1))
tappendcD_in_gaaa(X1, X2, X3, node(X1, X2, X4)) → U33_gaaa(X1, X2, X3, X4, tappendcB_in_gaa(X1, X3, X4))
U33_gaaa(X1, X2, X3, X4, tappendcB_out_gaa(X1, X3, X4)) → tappendcD_out_gaaa(X1, X2, X3, node(X1, X2, X4))
tappendcE_in_aa(X1, node(nil, X1, nil)) → tappendcE_out_aa(X1, node(nil, X1, nil))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tcA_in_ga(x1, x2)  =  s2tcA_in_ga(x1)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x1, x4)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x1, x4)
s2tcA_out_ga(x1, x2)  =  s2tcA_out_ga(x1, x2)
0  =  0
tappendcD_in_gaaa(x1, x2, x3, x4)  =  tappendcD_in_gaaa(x1)
nil  =  nil
tappendcD_out_gaaa(x1, x2, x3, x4)  =  tappendcD_out_gaaa(x1, x4)
U32_gaaa(x1, x2, x3, x4, x5)  =  U32_gaaa(x1, x5)
tappendcB_in_gaa(x1, x2, x3)  =  tappendcB_in_gaa(x1)
tappendcB_out_gaa(x1, x2, x3)  =  tappendcB_out_gaa(x1, x3)
U28_gaa(x1, x2, x3, x4, x5, x6)  =  U28_gaa(x1, x3, x6)
U29_gaa(x1, x2, x3, x4, x5, x6)  =  U29_gaa(x1, x3, x6)
U33_gaaa(x1, x2, x3, x4, x5)  =  U33_gaaa(x1, x5)
tappendcE_in_aa(x1, x2)  =  tappendcE_in_aa
tappendcE_out_aa(x1, x2)  =  tappendcE_out_aa(x2)
S2TA_IN_GA(x1, x2)  =  S2TA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

S2TA_IN_GA(s(X1), node(nil, X2, X3)) → S2TA_IN_GA(X1, X3)
S2TA_IN_GA(s(X1), node(X2, X3, X2)) → S2TA_IN_GA(X1, X2)
S2TA_IN_GA(s(X1), node(X2, X3, nil)) → S2TA_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
nil  =  nil
S2TA_IN_GA(x1, x2)  =  S2TA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S2TA_IN_GA(s(X1)) → S2TA_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • S2TA_IN_GA(s(X1)) → S2TA_IN_GA(X1)
    The graph contains the following edges 1 > 1

(27) YES